Notes (Week 7 Monday)

A transition system is a tuple

  (S,→)

 where  → ∈ S × S

Note: in the context of state machines (aka transition systems),
 → is *not* implication, it's "transitions to"

   x → y      "there is a transition from x to y"

For *unlabelled* transition systems,
 (S,→) counts as deterministic if:

  For every s ∈ S, there is at most one s' ∈ S
  such that
            s → s'

For *labelled* transition systems
 (S,L,→) counts as deterministic if:

  For every s ∈ S and l ∈ L, there is at most one s' ∈ S

        s -- l --> s'


  "If the program ever terminates, then y = x!"

is logically equivalent to:

  "The program will never reach a final state
   where y ≠ x!"

Labelled transition systems:
  Robert Kelley (mid 70s)
Safety and liveness (informal):
  Leslie Lamport (late 70s)
Safety and liveness (formal):
  Fred Schneider and Bowen Alpern

Q: Is the negation of a safety property always a liveness
   property and vice versa?
A: No.

To prove a safety property of the form
  "I will never reach the bad states"

- Find a property φ characterising (possibly overapproximating)
  the reachable states
- Show that the bad state does not satisfy φ
- Show that φ is preserved by the transition relation

   If φ(s)   and  s → s'    then φ(s')

^ This property φ we call an *invariant*


 while(Math.random() = 0) {
 }
 y := 0

This program is *partially correct for φ ≡ y=0*
We know that *if* we reach a final state,
  then y must have value 0 in that state.
*But* we aren't guaranteed to reach a final state


 total correctness
  =   partial correctness   +  termination
      ^ safety                 ^ liveness

You *can* conjure programs where termination is
 guaranteed, *but* there exists no measure.

In such situations, you instead exhibit a well-founded
 order, and show that that decreases.

  x := <generate a random natural number>
  while(x ≠ 0) {
    x := x - 1;
  }

Transition system model for this program

   S   =   ℕ ∪ {init}

   Transitions:

        ⋃n∈ℕ.{(n+1,n)} ∪ {(init,n)}

To prove termination let's make a WFO:

   (ℕ∪{ω},<)

    (where  n < ω   for all n ∈ ℕ)

 My measure:
   f(init) = ω
   f(n) = n

There's three situations where WFOs are useful in termination proofs:

- When no measure exists (see above)
- When a measure exists, but is annoying to write down
- When a measure exists, but you can't write it down
    battle of hercules and hydra
    ^ this will literally never happen in practice